Make short and enum symbols work - #88

Fixes #63.

The defect

short is listed among the supported symbol types - TypeCode.Int16 is in the sort mapping and
in both marshalling switches - but no theorem over a short could be solved. Two defects in
series, and neither was reachable while the other stood.

using var context = new Z3Context();
context.NewTheorem<Symbols<short, short>>().Where(t => t.X1 == 7).Where(t => t.X2 == 1).Solve();
// System.InvalidCastException: Unable to cast object of type 'Microsoft.Z3.IntExpr'
//                              to type 'Microsoft.Z3.RealExpr'

1. Translation. A short symbol is created with MkIntConst, so it is an IntExpr. C#
widens short to int for the comparison, and the visitor read that Convert node's target
type as telling it the operand's Z3 sort:

case TypeCode.Int32:
    return context.MkReal2Int((RealExpr)inner);   // inner is an IntExpr here

2. Marshalling. Behind it, TypeCode.Int16 shared the Int32 arm and returned an int,
which reflection refuses to write to a short member -
ArgumentException: Object of type 'System.Int32' cannot be converted to type 'System.Int16'.

Enums take the same route: an enum's TypeCode is that of its underlying type, so DayOfWeek is
Int32, gets an MkIntConst, and then fails identically. That was reported as a comment on #63
and is fixed here by the same change.

The change

The conversion arm now reads the operand, not the target. A widening onto a value Z3 already
holds at integer sort is a no-op; only a real needs converting:

case TypeCode.Int32 when inner.IsInt:
    return inner;
case TypeCode.Int32:
    return context.MkReal2Int((RealExpr)inner);

The Char arm three lines below already did exactly this. Whoever wrote it had the right idea and
did not carry it across.

TypeCode.Int16 gets its own marshalling arm, with a checked cast to short. That choice
is load-bearing and is pinned by a test - see below.

Also removed: the switch on the operand type immediately above, whose only two cases were empty
breaks. #63 guessed it was "possibly the vestige of an intended fix", which reads right - it
switches on exactly the thing the fix needed to consult, and then does nothing with it.

Enums need nothing on the marshalling side. #63's comment predicted a second defect there, by
analogy with short. There is not one: the model value is an int, and reflection converts an
int to an enum member on its own. Measured directly
(PropertyInfo.SetValue(new EnumEnvironment(), 1) succeeds) rather than assumed, and the mutation
matrix below shows it independently - reverting the marshalling arm fails nine tests, none of them
an enum one.

Why the cast is checked

The symbol is an unbounded MkIntConst. Nothing tells Z3 the value has to fit in 16 bits, so a
constraint written against the widened int can be satisfied by a number the member cannot hold:

int beyondShortRange = 40000;
context.NewTheorem<Symbols<short, int>>().Where(t => t.X1 == beyondShortRange).Solve();
// System.OverflowException

An unchecked cast wraps 40000 to -25536 - a wrong answer that looks like a right one. Measured
both ways. Throwing is the lesser of the two available evils; the better answer is to bound the
symbol so Z3 cannot pick the value at all, which is raised as #87. The behaviour is pinned so
that a later simplification to a plain cast fails rather than silently starting to wrap.

C# blocks the direct spelling - t.X1 == 40000 against a short is error CS0652 - so the repro
needs a variable. That is also why this went unnoticed.

What is deliberately not changed

The array-element copy of the Int16 arm (Theorem.cs:502) still shares the Int32 case. It
is unreachable behind #64 - a short[] dies earlier, in the visitor, because the array sort
mapping gives Int16 a MkBitVecSort(16) range while the scalar mapping uses IntSort:

InvalidCastException: Unable to cast object of type 'Microsoft.Z3.BitVecExpr' to type 'Microsoft.Z3.RealExpr'

So no test can cover a change there, and shipping an unverifiable edit seemed worse than recording
it. Noted on #64 for whoever fixes it.

#76 is untouched. It is the Double arm of the same switch and fails for the same reason one
arm along, and #76 suggests doing the two together. Confirmed still failing identically after this
change (RatNum to IntExpr), so this PR neither fixes nor disturbs it. Kept separate because
they are separate lines with separate repros, and #76 has no pin yet.

Enums with a non-int underlying type stay unsupported. A byte-backed enum is
TypeCode.Byte, which the sort mapping has never handled, so it stops at the guard that rejects a
bare byte or uint: NotSupportedException naming the member. That is the outcome #63 asked
for where a type genuinely is not supported, and it is now pinned.

Tests

202 -> 214.

The one that nearly did not work

Adding the guard dropped branch coverage by one. The branch it pointed at was the real-to-int
conversion: before this change that line was reachable only from a widening the visitor misread,
so every execution of it threw. It was covered without ever having worked, and no test
exercised a genuine (int) cast of a real symbol.

The first version of the test asserted (int)t.X1 == 3 on a double symbol. It passed - and
passed just as happily under a mutation that removed the guard entirely, because Z3 satisfies that
constraint with X1 = 3.0, where truncating and not truncating agree. The test now adds
t.X1 > 3.5, which the two readings disagree about: with the conversion the answer is a real in
(3.5, 4), and without it the theorem is unsatisfiable. Recorded because the weak version looked
exactly as convincing as the strong one.

Mutation results

The first two barely overlap in what they catch, which is the point: the two defects are
independent and each is covered on its own.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 214/214 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 78.2% -> 78.3% line (675 of 861), branch unchanged at 70.9% (460 of 648) - the guard's
  new branch is covered in both directions

New issue

#87 - a short symbol is not bounded to short's range, so Z3 can pick a value it cannot
hold. Includes what I could and could not reach for int: the same hole exists in principle,
IntNum.Int throws above int range, but I could not construct a theorem that gets there.

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. Nothing about the hold changes.